Paper 2023/778

Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)

Alex Ozdemir, Stanford University
Riad S. Wahby, Carnegie Mellon University
Fraser Brown, Carnegie Mellon University
Clark Barrett, Stanford University
Abstract

Zero Knowledge Proofs (ZKPs) are cryptographic protocols by which a prover convinces a verifier of the truth of a statement with- out revealing any other information. Typically, statements are expressed in a high-level language and then compiled to a low-level representation on which the ZKP operates. Thus, a bug in a ZKP compiler can com- promise the statement that the ZK proof is supposed to establish. This paper takes a step towards ZKP compiler correctness by partially veri- fying a field-blasting compiler pass, a pass that translates Boolean and bit-vector logic into equivalent operations in a finite field. First, we define correctness for field-blasters and ZKP compilers more generally. Next, we describe the specific field-blaster using a set of encoding rules and de- fine verification conditions for individual rules. Finally, we connect the rules and the correctness definition by showing that if our verification conditions hold, the field-blaster is correct. We have implemented our approach in the CirC ZKP compiler and have proved bounded versions of the corresponding verification conditions. We show that our partially verified field-blaster does not hurt the performance of the compiler or its output; we also report on four bugs uncovered during verification.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. CAV'23
Keywords
zero knowledgecompilersverificationfinite fields
Contact author(s)
aozdemir @ cs stanford edu
History
2023-05-30: revised
2023-05-27: received
See all versions
Short URL
https://ia.cr/2023/778
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2023/778,
      author = {Alex Ozdemir and Riad S. Wahby and Fraser Brown and Clark Barrett},
      title = {Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/778},
      year = {2023},
      url = {https://eprint.iacr.org/2023/778}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.